Report for Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/test-0521_true-valid-memsafety/test-0521_true-valid-memsafety.c (Counterexample 11)

Generated on 2025-08-28 16:16:53 by CPAchecker 4.0 / terminationAnalysis

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

Rank
Scope
-V-
{{line.bestrank}}
{{line.desc}}
Precondition (initial variable assignment):

{{precondition}}

{{fault.rank}}. {{fault.score}} Details:
Current values:
Name Value
1
extern void __VERIFIER_error() __attribute__ ((__noreturn__));  
2
  
3
typedef long unsigned int size_t;  
4
typedef int wchar_t;  
5
  
6
union wait  
7
  {  
8
    int w_status;  
9
    struct  
10
      {  
11
 unsigned int __w_termsig:7;  
12
 unsigned int __w_coredump:1;  
13
 unsigned int __w_retcode:8;  
14
 unsigned int:16;  
15
      } __wait_terminated;  
16
    struct  
17
      {  
18
 unsigned int __w_stopval:8;  
19
 unsigned int __w_stopsig:8;  
20
 unsigned int:16;  
21
      } __wait_stopped;  
22
  };  
23
typedef union  
24
  {  
25
    union wait *__uptr;  
26
    int *__iptr;  
27
  } __WAIT_STATUS __attribute__ ((__transparent_union__));  
28
  
29
typedef struct  
30
  {  
31
    int quot;  
32
    int rem;  
33
  } div_t;  
34
typedef struct  
35
  {  
36
    long int quot;  
37
    long int rem;  
38
  } ldiv_t;  
39
  
40
  
41
__extension__ typedef struct  
42
  {  
43
    long long int quot;  
44
    long long int rem;  
45
  } lldiv_t;  
46
  
47
extern size_t __ctype_get_mb_cur_max (void) __attribute__ ((__nothrow__ , __leaf__)) ;  
48
  
49
extern double atof (__const char *__nptr)  
50
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;  
51
extern int atoi (__const char *__nptr)  
52
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;  
53
extern long int atol (__const char *__nptr)  
54
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;  
55
  
56
  
57
__extension__ extern long long int atoll (__const char *__nptr)  
58
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;  
59
  
60
  
61
extern double strtod (__const char *__restrict __nptr,  
62
        char **__restrict __endptr)  
63
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
64
  
65
  
66
extern float strtof (__const char *__restrict __nptr,  
67
       char **__restrict __endptr) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
68
extern long double strtold (__const char *__restrict __nptr,  
69
       char **__restrict __endptr)  
70
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
71
  
72
  
73
extern long int strtol (__const char *__restrict __nptr,  
74
   char **__restrict __endptr, int __base)  
75
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
76
extern unsigned long int strtoul (__const char *__restrict __nptr,  
77
      char **__restrict __endptr, int __base)  
78
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
79
  
80
__extension__  
81
extern long long int strtoq (__const char *__restrict __nptr,  
82
        char **__restrict __endptr, int __base)  
83
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
84
__extension__  
85
extern unsigned long long int strtouq (__const char *__restrict __nptr,  
86
           char **__restrict __endptr, int __base)  
87
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
88
  
89
__extension__  
90
extern long long int strtoll (__const char *__restrict __nptr,  
91
         char **__restrict __endptr, int __base)  
92
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
93
__extension__  
94
extern unsigned long long int strtoull (__const char *__restrict __nptr,  
95
     char **__restrict __endptr, int __base)  
96
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
97
  
98
extern char *l64a (long int __n) __attribute__ ((__nothrow__ , __leaf__)) ;  
99
extern long int a64l (__const char *__s)  
100
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__pure__)) __attribute__ ((__nonnull__ (1))) ;  
101
  
102
typedef unsigned char __u_char;  
103
typedef unsigned short int __u_short;  
104
typedef unsigned int __u_int;  
105
typedef unsigned long int __u_long;  
106
typedef signed char __int8_t;  
107
typedef unsigned char __uint8_t;  
108
typedef signed short int __int16_t;  
109
typedef unsigned short int __uint16_t;  
110
typedef signed int __int32_t;  
111
typedef unsigned int __uint32_t;  
112
typedef signed long int __int64_t;  
113
typedef unsigned long int __uint64_t;  
114
typedef long int __quad_t;  
115
typedef unsigned long int __u_quad_t;  
116
typedef unsigned long int __dev_t;  
117
typedef unsigned int __uid_t;  
118
typedef unsigned int __gid_t;  
119
typedef unsigned long int __ino_t;  
120
typedef unsigned long int __ino64_t;  
121
typedef unsigned int __mode_t;  
122
typedef unsigned long int __nlink_t;  
123
typedef long int __off_t;  
124
typedef long int __off64_t;  
125
typedef int __pid_t;  
126
typedef struct { int __val[2]; } __fsid_t;  
127
typedef long int __clock_t;  
128
typedef unsigned long int __rlim_t;  
129
typedef unsigned long int __rlim64_t;  
130
typedef unsigned int __id_t;  
131
typedef long int __time_t;  
132
typedef unsigned int __useconds_t;  
133
typedef long int __suseconds_t;  
134
typedef int __daddr_t;  
135
typedef long int __swblk_t;  
136
typedef int __key_t;  
137
typedef int __clockid_t;  
138
typedef void * __timer_t;  
139
typedef long int __blksize_t;  
140
typedef long int __blkcnt_t;  
141
typedef long int __blkcnt64_t;  
142
typedef unsigned long int __fsblkcnt_t;  
143
typedef unsigned long int __fsblkcnt64_t;  
144
typedef unsigned long int __fsfilcnt_t;  
145
typedef unsigned long int __fsfilcnt64_t;  
146
typedef long int __ssize_t;  
147
typedef __off64_t __loff_t;  
148
typedef __quad_t *__qaddr_t;  
149
typedef char *__caddr_t;  
150
typedef long int __intptr_t;  
151
typedef unsigned int __socklen_t;  
152
typedef __u_char u_char;  
153
typedef __u_short u_short;  
154
typedef __u_int u_int;  
155
typedef __u_long u_long;  
156
typedef __quad_t quad_t;  
157
typedef __u_quad_t u_quad_t;  
158
typedef __fsid_t fsid_t;  
159
typedef __loff_t loff_t;  
160
typedef __ino_t ino_t;  
161
typedef __dev_t dev_t;  
162
typedef __gid_t gid_t;  
163
typedef __mode_t mode_t;  
164
typedef __nlink_t nlink_t;  
165
typedef __uid_t uid_t;  
166
typedef __off_t off_t;  
167
typedef __pid_t pid_t;  
168
typedef __id_t id_t;  
169
typedef __ssize_t ssize_t;  
170
typedef __daddr_t daddr_t;  
171
typedef __caddr_t caddr_t;  
172
typedef __key_t key_t;  
173
  
174
typedef __clock_t clock_t;  
175
  
176
  
177
  
178
typedef __time_t time_t;  
179
  
180
  
181
typedef __clockid_t clockid_t;  
182
typedef __timer_t timer_t;  
183
typedef unsigned long int ulong;  
184
typedef unsigned short int ushort;  
185
typedef unsigned int uint;  
186
typedef int int8_t __attribute__ ((__mode__ (__QI__)));  
187
typedef int int16_t __attribute__ ((__mode__ (__HI__)));  
188
typedef int int32_t __attribute__ ((__mode__ (__SI__)));  
189
typedef int int64_t __attribute__ ((__mode__ (__DI__)));  
190
typedef unsigned int u_int8_t __attribute__ ((__mode__ (__QI__)));  
191
typedef unsigned int u_int16_t __attribute__ ((__mode__ (__HI__)));  
192
typedef unsigned int u_int32_t __attribute__ ((__mode__ (__SI__)));  
193
typedef unsigned int u_int64_t __attribute__ ((__mode__ (__DI__)));  
194
typedef int register_t __attribute__ ((__mode__ (__word__)));  
195
typedef int __sig_atomic_t;  
196
typedef struct  
197
  {  
198
    unsigned long int __val[(1024 / (8 * sizeof (unsigned long int)))];  
199
  } __sigset_t;  
200
typedef __sigset_t sigset_t;  
201
struct timespec  
202
  {  
203
    __time_t tv_sec;  
204
    long int tv_nsec;  
205
  };  
206
struct timeval  
207
  {  
208
    __time_t tv_sec;  
209
    __suseconds_t tv_usec;  
210
  };  
211
typedef __suseconds_t suseconds_t;  
212
typedef long int __fd_mask;  
213
typedef struct  
214
  {  
215
    __fd_mask __fds_bits[1024 / (8 * (int) sizeof (__fd_mask))];  
216
  } fd_set;  
217
typedef __fd_mask fd_mask;  
218
  
219
extern int select (int __nfds, fd_set *__restrict __readfds,  
220
     fd_set *__restrict __writefds,  
221
     fd_set *__restrict __exceptfds,  
222
     struct timeval *__restrict __timeout);  
223
extern int pselect (int __nfds, fd_set *__restrict __readfds,  
224
      fd_set *__restrict __writefds,  
225
      fd_set *__restrict __exceptfds,  
226
      const struct timespec *__restrict __timeout,  
227
      const __sigset_t *__restrict __sigmask);  
228
  
229
  
230
__extension__  
231
extern unsigned int gnu_dev_major (unsigned long long int __dev)  
232
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));  
233
__extension__  
234
extern unsigned int gnu_dev_minor (unsigned long long int __dev)  
235
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));  
236
__extension__  
237
extern unsigned long long int gnu_dev_makedev (unsigned int __major,  
238
            unsigned int __minor)  
239
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__));  
240
  
241
typedef __blksize_t blksize_t;  
242
typedef __blkcnt_t blkcnt_t;  
243
typedef __fsblkcnt_t fsblkcnt_t;  
244
  
245
  
246
typedef __fsfilcnt_t fsfilcnt_t;  
247
typedef unsigned long int pthread_t;  
248
typedef union  
249
{  
250
  char __size[56];  
251
  long int __align;  
252
} pthread_attr_t;  
253
typedef struct __pthread_internal_list  
254
{  
255
  struct __pthread_internal_list *__prev;  
256
  struct __pthread_internal_list *__next;  
257
} __pthread_list_t;  
258
typedef union  
259
{  
260
  struct __pthread_mutex_s  
261
  {  
262
    int __lock;  
263
    unsigned int __count;  
264
    int __owner;  
265
    unsigned int __nusers;  
266
    int __kind;  
267
    int __spins;  
268
    __pthread_list_t __list;  
269
  } __data;  
270
  char __size[40];  
271
  long int __align;  
272
} pthread_mutex_t;  
273
typedef union  
274
{  
275
  char __size[4];  
276
  int __align;  
277
} pthread_mutexattr_t;  
278
typedef union  
279
{  
280
  struct  
281
  {  
282
    int __lock;  
283
    unsigned int __futex;  
284
    __extension__ unsigned long long int __total_seq;  
285
    __extension__ unsigned long long int __wakeup_seq;  
286
    __extension__ unsigned long long int __woken_seq;  
287
    void *__mutex;  
288
    unsigned int __nwaiters;  
289
    unsigned int __broadcast_seq;  
290
  } __data;  
291
  char __size[48];  
292
  __extension__ long long int __align;  
293
} pthread_cond_t;  
294
typedef union  
295
{  
296
  char __size[4];  
297
  int __align;  
298
} pthread_condattr_t;  
299
typedef unsigned int pthread_key_t;  
300
typedef int pthread_once_t;  
301
typedef union  
302
{  
303
  struct  
304
  {  
305
    int __lock;  
306
    unsigned int __nr_readers;  
307
    unsigned int __readers_wakeup;  
308
    unsigned int __writer_wakeup;  
309
    unsigned int __nr_readers_queued;  
310
    unsigned int __nr_writers_queued;  
311
    int __writer;  
312
    int __shared;  
313
    unsigned long int __pad1;  
314
    unsigned long int __pad2;  
315
    unsigned int __flags;  
316
  } __data;  
317
  char __size[56];  
318
  long int __align;  
319
} pthread_rwlock_t;  
320
typedef union  
321
{  
322
  char __size[8];  
323
  long int __align;  
324
} pthread_rwlockattr_t;  
325
typedef volatile int pthread_spinlock_t;  
326
typedef union  
327
{  
328
  char __size[32];  
329
  long int __align;  
330
} pthread_barrier_t;  
331
typedef union  
332
{  
333
  char __size[4];  
334
  int __align;  
335
} pthread_barrierattr_t;  
336
  
337
extern long int random (void) __attribute__ ((__nothrow__ , __leaf__));  
338
extern void srandom (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));  
339
extern char *initstate (unsigned int __seed, char *__statebuf,  
340
   size_t __statelen) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));  
341
  
342
  
343
extern char *setstate (char *__statebuf) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
344
  
345
  
346
  
347
  
348
  
349
  
350
  
351
struct random_data  
352
  {  
353
    int32_t *fptr;  
354
    int32_t *rptr;  
355
    int32_t *state;  
356
    int rand_type;  
357
    int rand_deg;  
358
    int rand_sep;  
359
    int32_t *end_ptr;  
360
  };  
361
  
362
extern int random_r (struct random_data *__restrict __buf,  
363
       int32_t *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
364
  
365
extern int srandom_r (unsigned int __seed, struct random_data *__buf)  
366
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));  
367
  
368
extern int initstate_r (unsigned int __seed, char *__restrict __statebuf,  
369
   size_t __statelen,  
370
   struct random_data *__restrict __buf)  
371
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2, 4)));  
372
  
373
extern int setstate_r (char *__restrict __statebuf,  
374
         struct random_data *__restrict __buf)  
375
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
376
  
377
  
378
  
379
  
380
  
381
  
382
extern int rand (void) __attribute__ ((__nothrow__ , __leaf__));  
383
  
384
extern void srand (unsigned int __seed) __attribute__ ((__nothrow__ , __leaf__));  
385
  
386
  
387
  
388
  
389
extern int rand_r (unsigned int *__seed) __attribute__ ((__nothrow__ , __leaf__));  
390
  
391
  
392
  
393
  
394
  
395
  
396
  
397
extern double drand48 (void) __attribute__ ((__nothrow__ , __leaf__));  
398
extern double erand48 (unsigned short int __xsubi[3]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
399
  
400
  
401
extern long int lrand48 (void) __attribute__ ((__nothrow__ , __leaf__));  
402
extern long int nrand48 (unsigned short int __xsubi[3])  
403
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
404
  
405
  
406
extern long int mrand48 (void) __attribute__ ((__nothrow__ , __leaf__));  
407
extern long int jrand48 (unsigned short int __xsubi[3])  
408
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
409
  
410
  
411
extern void srand48 (long int __seedval) __attribute__ ((__nothrow__ , __leaf__));  
412
extern unsigned short int *seed48 (unsigned short int __seed16v[3])  
413
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
414
extern void lcong48 (unsigned short int __param[7]) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
415
  
416
  
417
  
418
  
419
  
420
struct drand48_data  
421
  {  
422
    unsigned short int __x[3];  
423
    unsigned short int __old_x[3];  
424
    unsigned short int __c;  
425
    unsigned short int __init;  
426
    unsigned long long int __a;  
427
  };  
428
  
429
  
430
extern int drand48_r (struct drand48_data *__restrict __buffer,  
431
        double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
432
extern int erand48_r (unsigned short int __xsubi[3],  
433
        struct drand48_data *__restrict __buffer,  
434
        double *__restrict __result) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
435
  
436
  
437
extern int lrand48_r (struct drand48_data *__restrict __buffer,  
438
        long int *__restrict __result)  
439
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
440
extern int nrand48_r (unsigned short int __xsubi[3],  
441
        struct drand48_data *__restrict __buffer,  
442
        long int *__restrict __result)  
443
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
444
  
445
  
446
extern int mrand48_r (struct drand48_data *__restrict __buffer,  
447
        long int *__restrict __result)  
448
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
449
extern int jrand48_r (unsigned short int __xsubi[3],  
450
        struct drand48_data *__restrict __buffer,  
451
        long int *__restrict __result)  
452
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
453
  
454
  
455
extern int srand48_r (long int __seedval, struct drand48_data *__buffer)  
456
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));  
457
  
458
extern int seed48_r (unsigned short int __seed16v[3],  
459
       struct drand48_data *__buffer) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
460
  
461
extern int lcong48_r (unsigned short int __param[7],  
462
        struct drand48_data *__buffer)  
463
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2)));  
464
  
465
  
466
  
467
  
468
  
469
  
470
  
471
  
472
  
473
extern void *malloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;  
474
  
475
extern void *calloc (size_t __nmemb, size_t __size)  
476
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;  
477
  
478
  
479
  
480
  
481
  
482
  
483
  
484
  
485
  
486
  
487
extern void *realloc (void *__ptr, size_t __size)  
488
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__warn_unused_result__));  
489
  
490
extern void free (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));  
491
  
492
  
493
  
494
  
495
extern void cfree (void *__ptr) __attribute__ ((__nothrow__ , __leaf__));  
496
  
497
extern void *alloca (size_t __size) __attribute__ ((__nothrow__ , __leaf__));  
498
  
499
  
500
  
501
  
502
  
503
  
504
  
505
extern void *valloc (size_t __size) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__malloc__)) ;  
506
  
507
  
508
  
509
  
510
extern int posix_memalign (void **__memptr, size_t __alignment, size_t __size)  
511
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
512
  
513
  
514
  
515
  
516
extern void abort (void) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  
517
  
518
  
519
  
520
extern int atexit (void (*__func) (void)) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
521
  
522
extern int on_exit (void (*__func) (int __status, void *__arg), void *__arg)  
523
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
524
  
525
extern void exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  
526
  
527
  
528
extern void _Exit (int __status) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  
529
  
530
  
531
extern char *getenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
532
  
533
extern char *__secure_getenv (__const char *__name)  
534
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
535
extern int putenv (char *__string) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
536
extern int setenv (__const char *__name, __const char *__value, int __replace)  
537
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (2)));  
538
extern int unsetenv (__const char *__name) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
539
extern int clearenv (void) __attribute__ ((__nothrow__ , __leaf__));  
540
extern char *mktemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
541
extern int mkstemp (char *__template) __attribute__ ((__nonnull__ (1))) ;  
542
extern int mkstemps (char *__template, int __suffixlen) __attribute__ ((__nonnull__ (1))) ;  
543
extern char *mkdtemp (char *__template) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
544
  
545
extern int system (__const char *__command) ;  
546
  
547
extern char *realpath (__const char *__restrict __name,  
548
         char *__restrict __resolved) __attribute__ ((__nothrow__ , __leaf__)) ;  
549
typedef int (*__compar_fn_t) (__const void *, __const void *);  
550
  
551
extern void *bsearch (__const void *__key, __const void *__base,  
552
        size_t __nmemb, size_t __size, __compar_fn_t __compar)  
553
     __attribute__ ((__nonnull__ (1, 2, 5))) ;  
554
extern void qsort (void *__base, size_t __nmemb, size_t __size,  
555
     __compar_fn_t __compar) __attribute__ ((__nonnull__ (1, 4)));  
556
extern int abs (int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;  
557
extern long int labs (long int __x) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;  
558
  
559
__extension__ extern long long int llabs (long long int __x)  
560
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;  
561
  
562
extern div_t div (int __numer, int __denom)  
563
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;  
564
extern ldiv_t ldiv (long int __numer, long int __denom)  
565
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;  
566
  
567
  
568
__extension__ extern lldiv_t lldiv (long long int __numer,  
569
        long long int __denom)  
570
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__const__)) ;  
571
  
572
extern char *ecvt (double __value, int __ndigit, int *__restrict __decpt,  
573
     int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;  
574
extern char *fcvt (double __value, int __ndigit, int *__restrict __decpt,  
575
     int *__restrict __sign) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;  
576
extern char *gcvt (double __value, int __ndigit, char *__buf)  
577
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;  
578
extern char *qecvt (long double __value, int __ndigit,  
579
      int *__restrict __decpt, int *__restrict __sign)  
580
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;  
581
extern char *qfcvt (long double __value, int __ndigit,  
582
      int *__restrict __decpt, int *__restrict __sign)  
583
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4))) ;  
584
extern char *qgcvt (long double __value, int __ndigit, char *__buf)  
585
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3))) ;  
586
extern int ecvt_r (double __value, int __ndigit, int *__restrict __decpt,  
587
     int *__restrict __sign, char *__restrict __buf,  
588
     size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));  
589
extern int fcvt_r (double __value, int __ndigit, int *__restrict __decpt,  
590
     int *__restrict __sign, char *__restrict __buf,  
591
     size_t __len) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));  
592
extern int qecvt_r (long double __value, int __ndigit,  
593
      int *__restrict __decpt, int *__restrict __sign,  
594
      char *__restrict __buf, size_t __len)  
595
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));  
596
extern int qfcvt_r (long double __value, int __ndigit,  
597
      int *__restrict __decpt, int *__restrict __sign,  
598
      char *__restrict __buf, size_t __len)  
599
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (3, 4, 5)));  
600
  
601
extern int mblen (__const char *__s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ;  
602
extern int mbtowc (wchar_t *__restrict __pwc,  
603
     __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__)) ;  
604
extern int wctomb (char *__s, wchar_t __wchar) __attribute__ ((__nothrow__ , __leaf__)) ;  
605
extern size_t mbstowcs (wchar_t *__restrict __pwcs,  
606
   __const char *__restrict __s, size_t __n) __attribute__ ((__nothrow__ , __leaf__));  
607
extern size_t wcstombs (char *__restrict __s,  
608
   __const wchar_t *__restrict __pwcs, size_t __n)  
609
     __attribute__ ((__nothrow__ , __leaf__));  
610
  
611
extern int rpmatch (__const char *__response) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1))) ;  
612
extern int getsubopt (char **__restrict __optionp,  
613
        char *__const *__restrict __tokens,  
614
        char **__restrict __valuep)  
615
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1, 2, 3))) ;  
616
extern int getloadavg (double __loadavg[], int __nelem)  
617
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__nonnull__ (1)));  
618
  
619
extern int __VERIFIER_nondet_int(void);  
620
struct node {  
621
    int value;  
622
    struct node *next;  
623
};  
624
struct list {  
625
    struct node *slist;  
626
    struct list *next;  
627
};  
628
struct iterator {  
629
    struct list *list;  
630
    struct node *node;  
631
};  
632
int main()  
633
{  
634
    struct list *data = ((void *)0);  
635
    {  
636
      while (__VERIFIER_nondet_int())  
637
        {  
638
          struct node *node = malloc(sizeof *node);  
639
          if (!node)  
640
              abort();  
641
          node->next = ((void *)0);  
642
          node->value = __VERIFIER_nondet_int();  
643
          struct list *item = malloc(sizeof *item);  
644
          if (!item)  
645
              abort();  
646
          item->slist = node;  
647
          item->next = data;  
648
          data = item;  
649
        }  
650
    }  
651
    {  
652
      struct iterator iter;  
653
      {  
654
        struct list *list = data;  
655
        if ((iter.list = list))  
656
          iter.node = list->slist;  
657
      }  
658
      struct node *node;  
659
      {  
660
        if (!iter.list)  
661
          node = ((void *)0);  
662
        else {  
663
          struct node *current = iter.node;  
664
          if ((iter.node = current->next))  
665
            node = current;  
666
          else {  
667
            if ((iter.list = iter.list->next))  
668
              iter.node = iter.list->slist;  
669
            node = current;  
670
          }  
671
        }  
672
      }  
673
      while ((node))  
674
      {  
675
        {  
676
          if (!iter.list)  
677
            node = ((void *)0);  
678
          else {  
679
            struct node *current = iter.node;  
680
            if ((iter.node = current->next))  
681
              node = current;  
682
            else {  
683
              if ((iter.list = iter.list->next))  
684
                iter.node = iter.list->slist;  
685
              node = current;  
686
            }  
687
          }  
688
        }  
689
      }  
690
    }  
691
    {  
692
      struct list *list = data;  
693
      while (list && list->next) {  
694
        struct list *dst = ((void *)0);  
695
        while (list) {  
696
          struct list *next = list->next;  
697
          if (!next) {  
698
            list->next = dst;  
699
            dst = list;  
700
            break;  
701
          }  
702
          { struct node **dst = &list->slist;  
703
            struct node *sub1 = list->slist;  
704
            struct node *sub2 = next->slist;  
705
            while (sub1 || sub2) {  
706
              struct node ***pdst = &dst;  
707
              struct node **pdata;  
708
              if (!sub2 || (sub1 && __VERIFIER_nondet_int()))  
709
                pdata = &sub1;  
710
              else  
711
                pdata = &sub2;  
712
              struct node *node = *pdata;  
713
              *pdata = node->next;  
714
              node->next = ((void *)0);  
715
              **pdst = node;  
716
              *pdst = &node->next;  
717
            }  
718
          }  
719
          list->next = dst;  
720
          dst = list;  
721
          list = next->next;  
722
          free(next);  
723
        }  
724
        list = dst;  
725
      }  
726
      data = list;  
727
    }  
728
    {  
729
      struct iterator iter;  
730
      {  
731
        struct list *list = data;  
732
        if ((iter.list = list))  
733
          iter.node = list->slist;  
734
      }  
735
      struct node *node;  
736
      {  
737
        if (!iter.list)  
738
          node = ((void *)0);  
739
        else {  
740
          struct node *current = iter.node;  
741
          if ((iter.node = current->next))  
742
            node = current;  
743
          else {  
744
            if ((iter.list = iter.list->next))  
745
              iter.node = iter.list->slist;  
746
            node = current;  
747
          }  
748
        }  
749
      }  
750
      while ((node))  
751
      {  
752
        {  
753
          if (!iter.list)  
754
            node = ((void *)0);  
755
          else {  
756
            struct node *current = iter.node;  
757
            if ((iter.node = current->next))  
758
              node = current;  
759
            else {  
760
              if ((iter.list = iter.list->next))  
761
                iter.node = iter.list->slist;  
762
              node = current;  
763
            }  
764
          }  
765
        }  
766
      }  
767
    }  
768
    {  
769
      while (data) {  
770
        struct list *next = data->next;  
771
        struct node *node = data->slist;  
772
        while (node) {  
773
            struct node *snext = node->next;  
774
            free(node);  
775
            node = snext;  
776
        }  
777
        free(data);  
778
        data = next;  
779
      }  
780
    }  
781
    return 0;  
782
}  
DateTimeLevelComponentMessage
2025-08-2816:16:33:182INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2025-08-2816:16:33:263INFOCPAchecker.runCPAchecker 4.0 / terminationAnalysis (OpenJDK 64-Bit Server VM 17.0.15) started
2025-08-2816:16:33:282INFOCPAchecker.parseParsing CFA from file(s) "Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/test-0521_true-valid-memsafety/test-0521_true-valid-memsafety.c"
2025-08-2816:16:34:656INFOCoreComponentsFactory.createAlgorithmUsing Restarting Algorithm
2025-08-2816:16:34:677WARNINGCPAchecker.printConfigurationWarningsThe following configuration options were specified but are not used:
cpa.arg.lateMerge
counterexample.export.exportWitness
2025-08-2816:16:34:677INFOCPAchecker.runAlgorithmStarting analysis ...
2025-08-2816:16:34:687INFORestartAlgorithm.runLoading analysis 1 from file /cpachecker/config/components/combinations-parallel-termination.properties ...
2025-08-2816:16:34:726INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
ResourceLimitChecker.fromConfiguration
Using the following resource limits: Thread CPU-time limit of 300s
2025-08-2816:16:35:074INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21.
2025-08-2816:16:35:460INFOAnalysis /cpachecker/config/components/combinations-parallel-termination.properties
Parallel analysis 1
PredicateCPA
PredicateCPARefiner.<init>
Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2025-08-2816:16:35:473WARNINGCPAs.retrieveCPAOrFailWarning: Skipping one analysis because the configuration file /cpachecker/config/components/combinations-parallel-termination.properties is invalid (TerminationAlgorithm needs a TerminationCPA)
2025-08-2816:16:35:476INFORestartAlgorithm.runLoading analysis 1 from file /cpachecker/config/components/termination-recursion.properties ...
2025-08-2816:16:35:484INFONestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/cpachecker/config/components/termination-recursion.properties': 'termination.config' has two values 'terminationAnalysis.properties' and 'termination-recursion.properties'. Using 'termination-recursion.properties'.
2025-08-2816:16:35:507WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
FormulaManagerView.<init>
Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics.
2025-08-2816:16:35:510INFOAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
PredicateCPA.<init>
Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21.
2025-08-2816:16:35:717INFOAnalysis /cpachecker/config/components/termination-recursion.properties
PredicateCPA
PredicateCPARefiner.<init>
Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy.
2025-08-2816:16:35:785WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
FormulaManagerView.<init>
Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics.
2025-08-2816:16:35:820INFORestartAlgorithm.runStarting analysis 1 ...
2025-08-2816:16:35:821INFOAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.run0
Starting termination algorithm.
2025-08-2816:16:43:252WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
InequalityConverter.convert
Warning: Could not extract lasso (Loop with heads [N153]
incoming: [line 772: N152 -{while}-> N153]
outgoing: [line 772: N153 -{[node__4 == 0]}-> N155]
nodes: [N153, N154, N156, N157, N158]
). (Unknown sort in equality)
2025-08-2816:16:43:255WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2816:16:45:778WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
InequalityConverter.convert
Warning: Could not extract lasso (Loop with heads [N153]
incoming: [line 772: N152 -{while}-> N153]
outgoing: [line 772: N153 -{[node__4 == 0]}-> N155]
nodes: [N153, N154, N156, N157, N158]
). (Unknown sort in equality)
2025-08-2816:16:45:782WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2816:16:48:079WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
InequalityConverter.convert
Warning: Could not extract lasso (Loop with heads [N153]
incoming: [line 772: N152 -{while}-> N153]
outgoing: [line 772: N153 -{[node__4 == 0]}-> N155]
nodes: [N153, N154, N156, N157, N158]
). (Unknown sort in equality)
2025-08-2816:16:48:080WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2816:16:50:244WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
InequalityConverter.convert
Warning: Could not extract lasso (Loop with heads [N153]
incoming: [line 772: N152 -{while}-> N153]
outgoing: [line 772: N153 -{[node__4 == 0]}-> N155]
nodes: [N153, N154, N156, N157, N158]
). (Unknown sort in equality)
2025-08-2816:16:50:245WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2816:16:52:319WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
InequalityConverter.convert
Warning: Could not extract lasso (Loop with heads [N153]
incoming: [line 772: N152 -{while}-> N153]
outgoing: [line 772: N153 -{[node__4 == 0]}-> N155]
nodes: [N153, N154, N156, N157, N158]
). (Unknown sort in equality)
2025-08-2816:16:52:320WARNINGAnalysis /cpachecker/config/components/termination-recursion.properties
TerminationAlgorithm.proveLoopTermination
Could not synthesize a termination or non-termination argument.
2025-08-2816:16:52:644SEVERERefinementFailedException.forInterpolationFailureInSolverError: Refinement failed: Interpolation failed in solver MATHSAT5 with message 'uncolorable Array proof'.
Statistics NameStatistics ValueAdditional Value
Restart Algorithm statistics
Number of algorithms provided 2
Number of algorithms used 1
Last algorithm used /cpachecker/config/components/combinations-parallel-termination.properties
Total time for algorithm 1 17.957s
PredicateCPA statistics
Number of abstractions 380 3% of all post computations
Times abstraction was reused 0
Because of function entry/exit 0 0%
Because of loop head 366 96%
Because of join nodes 0 0%
Because of threshold 0 0%
Because of target state 14 4%
Times precision was empty 73 19%
Times precision was {false} 10 3%
Times result was cached 107 28%
Times cartesian abs was used 0 0%
Times boolean abs was used 190 50%
Times result was 'false' 41 11%
Number of strengthen sat checks 0
Number of coverage checks 8120
BDD entailment checks 737
Number of SMT sat checks 0
trivial 0
cached 0
Max ABE block size 62
Avg ABE block size 15.38 sum: 5846, count: 380, min: 0, max: 62
Number of predicates discovered 23
Number of abstraction locations 8
Max number of predicates per location 9
Avg number of predicates per location 6
Total predicates per abstraction 1483
Max number of predicates per abstraction 9
Avg number of predicates per abstraction 7.42
Number of irrelevant predicates 236 16%
Number of preds handled by boolean abs 784 53%
Total number of models for allsat 566
Max number of models for allsat 24
Avg number of models for allsat 2.98
Time for post operator 1.332s
Time for path formula creation 1.314s
Time for strengthen operator 0.035s
Time for prec operator 0.858s
Time for abstraction 0.794s Max: 0.016s, Count: 380
Boolean abstraction 0.405s
Solving time 0.221s Max: 0.007s
Model enumeration time 0.153s
Time for BDD construction 0.048s Max: 0.002s
Time for merge operator 0.048s
Time for coverage checks 0.012s
Time for BDD entailment checks 0.011s
Total time for SMT solver (w/o itp) 0.374s
Number of path formula cache hits 7183 50%
Inside post operator
Inside path formula creation
Time for path formula computation 1.269s
Total number of created targets for pointer analysis 0
Number of BDD nodes 1584
Size of BDD node table 466043
Size of BDD cache 46619
Size of BDD node cleanup queue 0.44 sum: 1121, count: 2540, min: 0, max: 356
Time for BDD node cleanup 0.004s
Time for BDD garbage collection 0.000s in 0 runs
KeyValue statistics
Init. function predicates 0
Init. global predicates 0
Init. location predicates 0
Invariant Generation statistics
AutomatonAnalysis (NonTerminationLabelAutomaton) statistics
Number of states 1
Total time for successor computation 0.052s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 11974, count: 11974, min: 1, max: 1 [1 x 11974]
Number of states with assumption transitions 0
AutomatonAnalysis (TerminatingFunctions) statistics
Number of states 1
Total time for successor computation 0.016s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 11938, count: 11974, min: 0, max: 1 [0 x 36, 1 x 11938]
Number of states with assumption transitions 0
Termination Algorithm statistics
Total time 16.822s
Time for recursion analysis 0.000s
Number of analysed loops 1 13%
Total time for loop analysis 16.817s
Avg time per loop analysis 16.817s
Max time per loop analysis 16.817s
Number of safety analysis runs 6
Avg safety analysis run per loop 6.00
Max safety analysis run per loop 6 for loops [N153]
Total time for safety analysis 4.667s
Avg time per safety analysis run 0.777s
Max time per safety analysis run 2.238s
Number of analysed lassos 0
Avg number of lassos per loop 0.00
Max number of lassos per loop 0 for loops
Avg number of lassos per iteration 0.00
Max number of lassos per iteration 0
Total time for lassos analysis 12.126s
Avg time per iteration 2.425s
Max time per iteration 5.183s
Time for lassos construction 12.126s
Avg time for lasso construction per iteration 2.425s
Max time for lasso construction per iteration 5.183s
Time for stem and loop construction 0.314s
Avg time for stem and loop construction per iteration 0.062s
Max time for stem and loop construction per iteration 0.214s
Time for lassos creation 11.792s
Avg time for lassos creation per iteration 2.358s
Max time for lassos creation per iteration 4.961s
Total time for non-termination analysis 0.000s
Avg time for non-termination analysis per lasso 0.000s
Max time for non-termination analysis per lasso 0.000s
Total time for termination analysis 0.000s
Avg time for termination analysis per lasso 0.000s
Max time for termination analysis per lasso 0.000s
Total number of termination arguments 0
Avg termination arguments per loop 0.00
Max termination arguments per loop 0 for loops
Counterexample-Check Algorithm statistics
Number of counterexample checks 0
Termination Algorithm statistics
Total time 16.822s
Time for recursion analysis 0.000s
Number of analysed loops 1 13%
Total time for loop analysis 16.817s
Avg time per loop analysis 16.817s
Max time per loop analysis 16.817s
Number of safety analysis runs 6
Avg safety analysis run per loop 6.00
Max safety analysis run per loop 6 for loops [N153]
Total time for safety analysis 4.667s
Avg time per safety analysis run 0.777s
Max time per safety analysis run 2.238s
Number of analysed lassos 0
Avg number of lassos per loop 0.00
Max number of lassos per loop 0 for loops
Avg number of lassos per iteration 0.00
Max number of lassos per iteration 0
Total time for lassos analysis 12.126s
Avg time per iteration 2.425s
Max time per iteration 5.183s
Time for lassos construction 12.126s
Avg time for lasso construction per iteration 2.425s
Max time for lasso construction per iteration 5.183s
Time for stem and loop construction 0.314s
Avg time for stem and loop construction per iteration 0.062s
Max time for stem and loop construction per iteration 0.214s
Time for lassos creation 11.792s
Avg time for lassos creation per iteration 2.358s
Max time for lassos creation per iteration 4.961s
Total time for non-termination analysis 0.000s
Avg time for non-termination analysis per lasso 0.000s
Max time for non-termination analysis per lasso 0.000s
Total time for termination analysis 0.000s
Avg time for termination analysis per lasso 0.000s
Max time for termination analysis per lasso 0.000s
Total number of termination arguments 0
Avg termination arguments per loop 0.00
Max termination arguments per loop 0 for loops
Counterexample-Check Algorithm statistics
Number of counterexample checks 0
Code Coverage
Function coverage 1.000
Visited lines 377
Total lines 380
Line coverage 0.992
Visited conditions 60
Total conditions 60
Condition coverage 1.000
CPAchecker general statistics
Number of program locations 412
Number of CFA edges (per node) 437 count: 412, min: 0, max: 2, avg: 1.06
Number of relevant variables 27
Number of functions 1
Number of loops (and loop nodes) 8 sum: 158, min: 5, max: 40, avg: 19.75
Size of reached set 543
Number of reached locations 121 29%
Avg states per location 4
Max states per location 12 at node N154
Number of reached functions 1 100%
Number of partitions 121
Avg size of partitions 4
Max size of partitions 12 with key N154
Number of target states 1
Size of final wait list 17
Time for analysis setup 1.396s
Time for loading CPAs 0.020s
Time for loading parser 0.211s
Time for CFA construction 1.123s
Time for parsing file(s) 0.394s
Time for AST to CFA 0.319s
Time for CFA sanity check 0.057s
Time for post-processing 0.208s
Time for loop structure 0.019s
Time for AST structure 0.000s
Time for CFA export 0.548s
Time for function pointers resolving 0.005s
Function calls via function pointers 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls 0 count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables 0.109s
Time for collecting variables 0.070s
Time for solving dependencies 0.004s
Time for building hierarchy 0.000s
Time for building classification 0.030s
Time for exporting data 0.005s
Time for Analysis 17.959s
CPU time for analysis 37.040s
Total time for CPAchecker 19.366s
Total CPU time for CPAchecker 39.470s
Time for statistics 0.198s
Time for Garbage Collector 0.222s in 122 runs
Garbage Collector(s) used PS MarkSweep, PS Scavenge
Used heap memory 126MB ( 120 MiB) max; 66MB ( 63 MiB) avg; 140MB ( 133 MiB) peak
Used non-heap memory 65MB ( 62 MiB) max; 56MB ( 54 MiB) avg; 67MB ( 64 MiB) peak
Used in PS Old Gen pool 44MB ( 42 MiB) max; 31MB ( 29 MiB) avg; 44MB ( 42 MiB) peak
Allocated heap memory 261MB ( 249 MiB) max; 254MB ( 242 MiB) avg
Allocated non-heap memory 68MB ( 65 MiB) max; 60MB ( 57 MiB) avg
Total process virtual memory 14914MB ( 14223 MiB) max; 14868MB ( 14179 MiB) avg
#Configuration NameConfiguration Value
1analysis.algorithm.termination true
2analysis.machineModel Linux64
3analysis.name terminationAnalysis
4analysis.programNames Benchmarks/TermCOMP/C/SV-COMP_Mixed_Categories/test-0521_true-valid-memsafety/test-0521_true-valid-memsafety.c
5analysis.restartAfterUnknown true
6counterexample.export.exportWitness false
7cpa.arg.lateMerge prevent
8language C
9log.level INFO
10parser.usePreprocessor true
11restartAlgorithm.configFiles components/combinations-parallel-termination.properties, components/termination-recursion.properties::if-recursive
12specification
13statistics.print true
14termination.config terminationAnalysis.properties

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

{{dependency.name}} {{dependency.version}}

Source: {{dependency.repository}}

{{dependency.copyright}}

License:

Full text of license
{{dependencies.licenses[dependency.licenseId]}}